a, b:, E:({a..b}), i:.
a  j < b. E(j) * delta(i;j) = if a z i  i <z b then E(i) else 0 fi    

latex

Definitions

Y, t.2, t.1, 0, +r, e, *, (op,id) lb  i < ub. E(i), r+gp,  lb  i < ub. E(i), <+*>, (r) i  k < j. E(k), a  j < b. E(j), SQType(T), False, delta(i;j), {T}, suptype(S; T), S  T, P  Q, A, A c B, True, T, ff, P  Q, P & Q, P  Q, tt, i  j < k, x. t(x), , {i...}, t  T, p  q, if b then t else f fi , x(s), {i..j}, A  B, P  Q, x:A. B(x), Dec(P), Unit, ,

Lemmas

decidable le, qmul one qrng, mon ident q, qadd comm q, qmul zero qrng, not functionality wrt iff, assert of bnot, assert of eq int, bool sq, bool cases, int inc rationals, not wf, eq int wf, qadd wf, sum unroll hi q, band wf, sum unroll base q, int upper ind, int le to int upper, rationals wf, or functionality wrt iff, assert of bor, bnot of lt int, bnot thru band, true wf, squash wf, le int wf, bor wf, and functionality wrt iff, assert of band, false wf, bfalse wf, assert of lt int, bnot of le int, eqff to assert, bnot wf, lt int wf, assert of le int, eqtt to assert, le wf, assert wf, iff transitivity, bool wf, int seg wf, delta wf, int-rational, qmul wf, qsum wf